$\forall$$A$:es\_realizer\{i:l\}, $i$:Id.
\\[0ex]($\neg$($\uparrow$R{-}has{-}loc($A$; $i$))) $\Rightarrow$ (R{-}da($A$; $i$) = fpf{-}empty $\in$ fpf(Knd; $k$.Type))